Nuprl Definition : Rusends1 0,22

k(v) sends [tg,f(State(ds), v)] on l
== sends k(v:A) on l:
== tagged([<tg,s,v. [f(s,v)]>],State(ds),v):tg : T 
latex



clarification:

Rusends1(ds;k;A;l;tg;T;f)
== sends k(v:A) on l:
== tagged(<tg,s,v. (f(s,v)).nil>.nil,State(ds),v):tg : T 
latex


Definitionssends knd(v:T) on l:tagged(g,State(ds),v):dt, x : v, <a,b>, x.A(x), car.cdr, f(a), nil
FDL editor aliasesRusends1

origin